i:Id, T:Type, v:T, x:Id.
@i: x:T initially x = v realizes es. vartype(i;x)  T & x initially@i  = v 

latex

Definitions

t  T, IdDeq, Id, x:A. B(x), f(x), mk-ma, x : v, x  dom(f), f(x)?z, x : t initially x = v, M.ds(x), M(i), @i: x:T initially x = v, vartype(i;x), A & B, Action(i), x:AB(x), P  Q, IdLnk, True, b, , #$n, AB, a<b, Void, False, A, {x:A| B(x) }, , x:AB(x), P & Q, {T}, z != f(x)  P(a;z), M.bframe(k sends on l), M.aframe(k affects x), M.sframe(k sends <l,tg>), M.frame(k affects x), M.send(k;l;s;v;ms;i), M.ef(k,x,s,v,w), M.pre(a,s,v), M.init(x,v), PossibleWorld(D;w), s.x, es_init(es), es-T(es), x initially@i , ES(the_w), vartype(i;x), s = t, FairFifo, World, D realizes2 es.P(es), Type, Prop, x:A. B(x), es is an event system of D, ES, x.A(x), x. t(x), D realizes es. P(es)

Lemmas

d-realizes2-implies-realizes, event system wf, d-es wf, es-vartype wf, es-initially wf, world wf, fair-fifo wf, possible-world wf, d-single-init wf, le wf, eqof eq btrue, Id wf, id-deq wf